package alloy.transform;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.ElemIntFormula;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.Formula;
import alloy.ast.Id;
import alloy.ast.IntCompOp;
import alloy.ast.IntExpr;
import alloy.ast.IntExprCastExpr;
import alloy.ast.LeafExpr;
import alloy.ast.Location;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.Qualifiers;
import alloy.ast.SetMultExpr;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.semantic.LocalScope;
import alloy.type.SigType;

public class DesugarIntExprCastExprVisitor extends ASTDepthFirstReplacer {

    public Object visit(IntExprCastExpr castExpr_) {
        
        // recursively replace anything inside (to fend off inputs like Int int Int a)
        visit((Node)castExpr_);

        //transforms Int i into { e: Int | e in Int && int e = i }
        // the "e in Int" is necessary for correct translation

        SigType intType = castExpr_.getType().toRelationType().getSigType();

        IntExpr valIntExpr = castExpr_.getIntExpr();

        Location loc = castExpr_.getLocation();
        Qualifiers quals = new Qualifiers(loc);
        Variable v = new Variable(castExpr_.getLocation(), new Id(loc, "e"), true);
        Variables vars = new Variables(loc);
        vars.addVariable(v);

        VariableExpr varExpr = new VariableExpr(loc, v);
        varExpr.setType(castExpr_.getType());

        LeafExpr intSigExpr = intType.toExpr();
        intSigExpr.setLeafId(intType.getSignature().getLeafId());

        ExprCastIntExpr varIntExpr = new ExprCastIntExpr(loc, varExpr);

        /* subset constraint no longer needed because this visitor is run before DesugarDeclsVisitor
        Formula form =
            new ElemFormula(
                loc,
                (VariableExpr)varExpr.copy(),
                new CompOp(loc, CompOp.SUBSETCOLON, false),
                intSigExpr);
        form =
            form.and(*/

        Formula form =
            new ElemIntFormula(loc, varIntExpr, IntCompOp.INT_EQUALS, valIntExpr);

        MultiplicityExpr multExpr =
            new SetMultExpr(loc, Multiplicity.NONE, intSigExpr);
        multExpr.setType(castExpr_.getType());

        Decl decl = new Decl(loc, quals, vars, multExpr);
        Decls decls = new Decls(loc);
        decls.addDecl(decl);

        ComprehensionExpr compExpr = new ComprehensionExpr(castExpr_.getLocation(), decls, form, false);
        compExpr.annotate("desugared IntExprCastExpr");
        compExpr.setType(castExpr_.getType());
        compExpr.setLocalScope(LocalScope.genScopeFromDecls(decls));

        return compExpr;
    }
}
